\begin{tabbing}
(let T = Unfold `bool` 
\\[0ex]i\=n \=\+\+
\\[0ex]((((((((((T 1) 
\-\\[0ex]CollapseTHEN (T 2))$\cdot$) 
\\[0ex]CollapseTHEN (T 3
\-\\[0ex])\=)$\cdot$) \+
\\[0ex]CollapseTHEN (ApFunToHypEquands `z' case $z$ of inl($x$) =$>$ $x$ $\mid$ inr($x$) =$>$ $x$ Unit 3))$\cdot$)
\\[0ex]
\\[0ex]CollapseTHENM (ApFunToHypEquands `z' case $z$ of inl($x$) =$>$ True $\mid$ inr($x$) =$>$ False $\mathbb{P}_{1}$ 3))$\cdot$
\-\\[0ex])\= \+
\\[0ex]CollapseTHENA ((Auto\_aux (first\_nat 1:n) ((first\_nat 1:n),(first\_nat 3:n)) (first\_tok 
\-\\[0ex]:t) inil\_term)))$\cdot$)
\end{tabbing}